merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
↳ QTRS
↳ Overlay + Local Confluence
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
merge(nil, x0)
merge(x0, nil)
merge(.(x0, x1), .(x2, x3))
++(nil, x0)
++(.(x0, x1), x2)
if(true, x0, x1)
if(false, x0, x1)
MERGE(.(x, y), .(u, v)) → MERGE(y, .(u, v))
MERGE(.(x, y), .(u, v)) → IF(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
MERGE(.(x, y), .(u, v)) → MERGE(.(x, y), v)
++1(.(x, y), z) → ++1(y, z)
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
merge(nil, x0)
merge(x0, nil)
merge(.(x0, x1), .(x2, x3))
++(nil, x0)
++(.(x0, x1), x2)
if(true, x0, x1)
if(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
MERGE(.(x, y), .(u, v)) → MERGE(y, .(u, v))
MERGE(.(x, y), .(u, v)) → IF(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
MERGE(.(x, y), .(u, v)) → MERGE(.(x, y), v)
++1(.(x, y), z) → ++1(y, z)
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
merge(nil, x0)
merge(x0, nil)
merge(.(x0, x1), .(x2, x3))
++(nil, x0)
++(.(x0, x1), x2)
if(true, x0, x1)
if(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
MERGE(.(x, y), .(u, v)) → IF(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
MERGE(.(x, y), .(u, v)) → MERGE(y, .(u, v))
MERGE(.(x, y), .(u, v)) → MERGE(.(x, y), v)
++1(.(x, y), z) → ++1(y, z)
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
merge(nil, x0)
merge(x0, nil)
merge(.(x0, x1), .(x2, x3))
++(nil, x0)
++(.(x0, x1), x2)
if(true, x0, x1)
if(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
++1(.(x, y), z) → ++1(y, z)
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
merge(nil, x0)
merge(x0, nil)
merge(.(x0, x1), .(x2, x3))
++(nil, x0)
++(.(x0, x1), x2)
if(true, x0, x1)
if(false, x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
++1(.(x, y), z) → ++1(y, z)
.2 > ++^11
++^11: multiset
.2: multiset
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
merge(nil, x0)
merge(x0, nil)
merge(.(x0, x1), .(x2, x3))
++(nil, x0)
++(.(x0, x1), x2)
if(true, x0, x1)
if(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
MERGE(.(x, y), .(u, v)) → MERGE(y, .(u, v))
MERGE(.(x, y), .(u, v)) → MERGE(.(x, y), v)
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
merge(nil, x0)
merge(x0, nil)
merge(.(x0, x1), .(x2, x3))
++(nil, x0)
++(.(x0, x1), x2)
if(true, x0, x1)
if(false, x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MERGE(.(x, y), .(u, v)) → MERGE(.(x, y), v)
Used ordering: Combined order from the following AFS and order.
MERGE(.(x, y), .(u, v)) → MERGE(y, .(u, v))
.2 > MERGE1
.2: [2,1]
MERGE1: multiset
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
MERGE(.(x, y), .(u, v)) → MERGE(y, .(u, v))
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
merge(nil, x0)
merge(x0, nil)
merge(.(x0, x1), .(x2, x3))
++(nil, x0)
++(.(x0, x1), x2)
if(true, x0, x1)
if(false, x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MERGE(.(x, y), .(u, v)) → MERGE(y, .(u, v))
MERGE2 > .1
.1: [1]
MERGE2: multiset
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x
merge(nil, x0)
merge(x0, nil)
merge(.(x0, x1), .(x2, x3))
++(nil, x0)
++(.(x0, x1), x2)
if(true, x0, x1)
if(false, x0, x1)